A:Type, d1, d2, d3, d4:EqDecider(A), B:(AType), f, g:a:A fp B(a), x:A, z:B(x).
f  g  x  dom(f)  f(x)?z = g(x)?z  B(x) 

latex

Definitions	False, A & B, {T}, f  g, EqDecider(T), f(x)?z, if b t else f fi, Unit, P  Q, P & Q, P  Q, x  dom(f), a:A fp B(a), Top, x. t(x), f(x), , Prop, b, x(s), A, t  T, b, x:A. B(x)
Lemmas	assert wf, not wf, bnot wf, fpf-trivial-subtype-top, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool wf, deq wf, fpf wf, fpf-sub wf, fpf-dom functionality2, fpf-ap functionality